i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), snd:msg-spec(ds;da), T:Type.
(k:Knd. (k  ecl-trans-ks(ecl-trans(A)))  k  dom(da))
 "ecl"  dom(ds)
 T = ecl-trans-type(ecl-trans(A))
 ecl-machine1{ecl:ut2}
 ecl-machine1(i; ds; da; A) ||
 eecl-machine3(ds;da;"ecl";T;ecl-trans-ks(ecl-trans(A));ecl-trans-a(ecl-trans(A));snd) 

latex

Definitions

x:A. B(x), Id, P  Q, ecl-trans-ks(v), "$x", ecl-trans-type(A), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine3(ds;da;x;T;ks;a;snd), ecl-trans-a(v), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), R-state-var-init(i;ds;da;x;T;v;ks;tr), t  T, Valtype(da;k), 1of(t), x(s), x. t(x), Prop, A & B, S  T, S  T, P & Q, Top, T, True, Knd, (x  l), ecl-trans-tuple{i:l}(ds;da), State(ds), P  Q, x:A. B(x), P  Q

Lemmas

ecl-trans wf, ecl-trans-tuple wf, R-compat-Rall, IdLnk wf, remove-repeats wf, idlnk-deq wf, msg-spec-links wf, l member wf, R-lnk-tags wf, fpf-join wf, fpf-single wf, id-deq wf, ecl-tags wf, ecl-m3 wf, nat wf, decl-state wf, ma-valtype wf, bool wf, Rplus wf, R-state-var wf, fpf-compatible-single, Rinit wf, R-compat-Rplus-sq, R-state-var-lnk-tags-compat2, fpf-cap wf, Kind-deq wf, rcv wf, squash wf, true wf, fpf wf, Id wf, deq wf, subtype rel self, fpf-cap-void-subtype, fpf-compatible-join, fpf-compatible-join2, fpf-compatible-self, fpf-compatible-single2, fpf-compatible-singles, Rinit-lnk-tags-compat, assert wf, fpf-dom wf, fpf-trivial-subtype-top, ecl-trans-type wf, not wf, Knd wf, ecl-trans-ks wf, msg-spec wf, ecl wf